ArchiTRIO : A UML-compatible language for architectural description and its formal semanticsPRADELLA, Matteo; ROSSI, Matteo; MANDRIOLI, Dino et al.Lecture notes in computer science. 2005, pp 381-395, issn 0302-9743, isbn 3-540-29189-X, 1Vol, 15 p.Conference Paper

Advertising formal methods and organizing their teaching: Yes, but ..MANDRIOLI, Dino.Lecture notes in computer science. 2004, pp 214-224, issn 0302-9743, isbn 3-540-23611-2, 11 p.Conference Paper

The challenges of software engineering educationGHEZZI, Carlo; MANDRIOLI, Dino.Lecture notes in computer science. 2006, pp 115-127, issn 0302-9743, isbn 978-3-540-68203-5, 1Vol, 13 p.Conference Paper

FME 2003 : formal methods (Pisa, 8-14 September 2003)Araki, Keijiro; Gnesi, Stefania; Mandrioli, Dino et al.Lecture notes in computer science. 2003, issn 0302-9743, isbn 3-540-40828-2, XVII, 942 p, isbn 3-540-40828-2Conference Proceedings

program checking with certificates: Separating correctness-critical codeGLESNER, Sabine.Lecture notes in computer science. 2003, pp 758-777, issn 0302-9743, isbn 3-540-40828-2, 20 p.Conference Paper

On failures and faultsRANDELL, Brian.Lecture notes in computer science. 2003, pp 18-39, issn 0302-9743, isbn 3-540-40828-2, 22 p.Conference Paper

Composing invariantsCHARPENTIER, Michel.Lecture notes in computer science. 2003, pp 401-421, issn 0302-9743, isbn 3-540-40828-2, 21 p.Conference Paper

Improving JML: For a safer and more effective languageCHALIN, Patrice.Lecture notes in computer science. 2003, pp 440-461, issn 0302-9743, isbn 3-540-40828-2, 22 p.Conference Paper

A topological characterization of TCP/IP securityVIGNA, Giovanni.Lecture notes in computer science. 2003, pp 914-940, issn 0302-9743, isbn 3-540-40828-2, 27 p.Conference Paper

Combining real-time model-checking and fault tree analysisSCHÄFER, Andreas.Lecture notes in computer science. 2003, pp 522-541, issn 0302-9743, isbn 3-540-40828-2, 20 p.Conference Paper

Compositional verification of an ATM protocolRUSU, Vlad.Lecture notes in computer science. 2003, pp 223-243, issn 0302-9743, isbn 3-540-40828-2, 21 p.Conference Paper

Proving the correctness of Simpson's 4-Slot ACM using an assertional rely-guarantee proof methodHENDERSON, Neil.Lecture notes in computer science. 2003, pp 244-263, issn 0302-9743, isbn 3-540-40828-2, 20 p.Conference Paper

Using abstractions for heuristic state space exploration of reactive object-oriented systemsLETTRARI, Marc.Lecture notes in computer science. 2003, pp 462-481, issn 0302-9743, isbn 3-540-40828-2, 20 p.Conference Paper

Modeling Time in Computing: A Taxonomy and a Comparative SurveyFURIA, Carlo A; MANDRIOLI, Dino; MORZENTI, Angelo et al.ACM computing surveys. 2010, Vol 42, Num 2, issn 0360-0300, 1667063.1-1667063.59Article

Generating counterexamples for multi-valued model-checkingGURFINKEL, Arie; CHECHIK, Marsha.Lecture notes in computer science. 2003, pp 503-521, issn 0302-9743, isbn 3-540-40828-2, 19 p.Conference Paper

Synthesis and verification of constraints in the PGM protocolBOYER, Marc; SIGHIREANU, Mihaela.Lecture notes in computer science. 2003, pp 264-281, issn 0302-9743, isbn 3-540-40828-2, 18 p.Conference Paper

Lessons learned from a successful implementation of formal methods in an industrial projectWASSYNG, Alan; LAWFORD, Mark.Lecture notes in computer science. 2003, pp 133-153, issn 0302-9743, isbn 3-540-40828-2, 21 p.Conference Paper

Design of an automatic prover dedicated to the refinement of database applicationsMAMMAR, Amel; LALEAU, Régine.Lecture notes in computer science. 2003, pp 834-854, issn 0302-9743, isbn 3-540-40828-2, 21 p.Conference Paper

Reification of executable test scripts in formal specification-based test generation: The Java Card Transaction mechanism case studyBOUQUET, Fabrice; LEGEARD, Bruno.Lecture notes in computer science. 2003, pp 778-795, issn 0302-9743, isbn 3-540-40828-2, 18 p.Conference Paper

Event based sequential program development: Application to constructing a pointer programABRIAL, Jean-Raymond.Lecture notes in computer science. 2003, pp 51-74, issn 0302-9743, isbn 3-540-40828-2, 24 p.Conference Paper

Computing meta-transitions for linear transition systems with polynomialsMUSSET, Julien; RUSINOWITCH, Michaël.Lecture notes in computer science. 2003, pp 562-581, issn 0302-9743, isbn 3-540-40828-2, 20 p.Conference Paper

Refinement and verification of synchronized component-based systemsKOUCHNARENKO, Olga; LANOIX, Arnaud.Lecture notes in computer science. 2003, pp 341-358, issn 0302-9743, isbn 3-540-40828-2, 18 p.Conference Paper

Structuring retrenchments in B by decompositionPOPPLETON, Michael; BANACH, Richard.Lecture notes in computer science. 2003, pp 814-833, issn 0302-9743, isbn 3-540-40828-2, 20 p.Conference Paper

A general approach to deadlock freedom verification for software architecturesALDINI, Alessandro; BERNARDO, Marco.Lecture notes in computer science. 2003, pp 658-677, issn 0302-9743, isbn 3-540-40828-2, 20 p.Conference Paper

Model checking ftaTHUMS, Andreas; SCHELLHORN, Gerhard.Lecture notes in computer science. 2003, pp 739-757, issn 0302-9743, isbn 3-540-40828-2, 19 p.Conference Paper